Nuprl Definition : es-x-equiv
0,22
postcript
pdf
s1
s2
mod
x
@
i
==
z
:Id.
z
=
x
s1
(
z
) =
s2
(
z
)
latex
clarification:
es-x-equiv(
es
;
i
;
x
;
s1
;
s2
) ==
z
:Id.
z
=
x
Id
s1
(
z
) =
s2
(
z
)
es-vartype(
es
;
i
;
z
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
A
,
Id
,
s
=
t
,
vartype(
i
;
x
)
,
f
(
a
)
FDL editor aliases
es-x-equiv
origin